Termination proof of /tmp/tmpDN6yQ9/MainGet.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1870 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 890 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 180 ms)

        ↳9 AND

            ↳10 IDP

                ↳11 IDependencyGraphProof (⇔, 0 ms)

                ↳12 TRUE

            ↳13 IDP

                ↳14 IDependencyGraphProof (⇔, 0 ms)

                ↳15 TRUE

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 500 ms)

        ↳18 IDP

        ↳19 IDPtoQDPProof (⇒, 30 ms)

        ↳20 QDP

        ↳21 UsableRulesProof (⇔, 0 ms)

        ↳22 QDP

        ↳23 QReductionProof (⇔, 0 ms)

        ↳24 QDP

        ↳25 QDPSizeChangeProof (⇔, 0 ms)

        ↳26 YES

    ↳27 JBCTerminationSCC

        ↳28 SCCToIDPv1Proof (⇒, 1100 ms)

        ↳29 IDP

        ↳30 IDPNonInfProof (⇒, 130 ms)

        ↳31 IDP

        ↳32 IDependencyGraphProof (⇔, 0 ms)

        ↳33 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: DoublyLinkedList/MainGet

package DoublyLinkedList;

/**
 * A linked list with pointers to the previous and next elements
 * @author cotto
 */
public class DoublyLinkedList {
    public int value;
    public DoublyLinkedList prev;
    public DoublyLinkedList next;

    public DoublyLinkedList(final int v) {
        this.value = v;
    }

    public DoublyLinkedList getFirst() {
        if (this.prev == null) {
            return this;
        }
        return this.prev.getFirst();
    }

    public void move(final int relativePosition) {
        if (relativePosition == 0) {
            return;
        }
        if (relativePosition > 0 && this.next != null) {
            final DoublyLinkedList temp = this.next;
            if (this.prev != null) {
                this.prev.next = temp;
            }
            temp.prev = this.prev;
            this.next = temp.next;
            temp.next = this;
            this.prev = temp;
            move(relativePosition - 1);
        }
        if (relativePosition < 0 && this.prev != null) {
            final DoublyLinkedList temp = this.prev;
            if (this.next != null) {
                this.next.prev = temp;
            }
            temp.next = this.next;
            this.prev = temp.prev;
            temp.prev = this;
            this.next = temp;
            move(relativePosition - 1);
        }
    }

    public DoublyLinkedList get(final int index) {
        return this.getFirst().getR(index);
    }

    private DoublyLinkedList getR(final int index) {
      if (index == 0 || this.next == null) {
        return this;
      }
      return this.next.getR(index - 1);
    }

    public DoublyLinkedList find(final int v) {
        final DoublyLinkedList first = this.getFirst();
        return first.findR(v);
    }

    private DoublyLinkedList findR(final int v) {
        if (this.value == v) {
            return this;
        }
        if (this.next != null) {
            return this.next.findR(v);
        }
        return null;
    }

    public void delete(final int v) {
        final DoublyLinkedList elem = find(v);
        if (elem != null) {
            if (elem.prev != null) {
                elem.prev.next = elem.next;
            }
            if (elem.next != null) {
                elem.next.prev = elem.prev;
            }
        }
    }

    public DoublyLinkedList copy() {
        final DoublyLinkedList first = this.getFirst();
        return first.copyR(null);
    }

    private DoublyLinkedList copyR(final DoublyLinkedList p) {
        final DoublyLinkedList copy = new DoublyLinkedList(this.value);
        copy.prev = p;
        if (p != null) {
            p.next = copy;
        }
        if (this.next != null) {
            this.next.copyR(copy);
        }
        return copy;
    }

    static DoublyLinkedList createList() {
        final int count = Random.random();
        DoublyLinkedList cur = null;
        for (int i = 0; i < count; i++) {
            final DoublyLinkedList old = cur;
            cur = new DoublyLinkedList(Random.random());
            cur.prev = old;
            if (old != null) {
              old.next = cur;
            }
        }

        return cur;
    }
}


package DoublyLinkedList;

/**
 *
 * @author cotto
 */
public class MainGet {
    public static void main(final String[] args) {
        Random.args = args;
        final DoublyLinkedList list = DoublyLinkedList.createList();
        list.get(Random.random());
    }
}


package DoublyLinkedList;
public class Random {
    static String[] args;
    static int index = 0;

    public static int random() {
        if (args.length <= index) {
            return 0;
        }
        final String string = args[index];
        index++;
        if (string == null) {
            return 0;
        }
        return string.length();
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
DoublyLinkedList.MainGet.main([Ljava/lang/String;)V: Graph of 261 nodes with 0 SCCs.

DoublyLinkedList.DoublyLinkedList.createList()LDoublyLinkedList/DoublyLinkedList;: Graph of 166 nodes with 1 SCC.

DoublyLinkedList.DoublyLinkedList.getFirst()LDoublyLinkedList/DoublyLinkedList;: Graph of 56 nodes with 0 SCCs.

DoublyLinkedList.DoublyLinkedList.getR(I)LDoublyLinkedList/DoublyLinkedList;: Graph of 72 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DoublyLinkedList.DoublyLinkedList.getR(I)LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods: DoublyLinkedList.DoublyLinkedList.getR(I)LDoublyLinkedList/DoublyLinkedList;
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 33 rules for P and 43 rules for R.

P rules:
3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(o2057sub), i1414, i1414) → 3195_0_getR_EQ(EOS(STATIC_3195), java.lang.Object(o2057sub), i1414, i1414)
3195_0_getR_EQ(EOS(STATIC_3195), java.lang.Object(o2057sub), i1414, i1414) → 3202_0_getR_Load(EOS(STATIC_3202), java.lang.Object(o2057sub), i1414) | >(i1414, 0)
3202_0_getR_Load(EOS(STATIC_3202), java.lang.Object(o2057sub), i1414) → 3211_0_getR_FieldAccess(EOS(STATIC_3211), java.lang.Object(o2057sub), i1414, java.lang.Object(o2057sub))
3211_0_getR_FieldAccess(EOS(STATIC_3211), java.lang.Object(o2057sub), i1414, java.lang.Object(o2057sub)) → 3226_0_getR_FieldAccess(EOS(STATIC_3226), java.lang.Object(o2057sub), i1414, java.lang.Object(o2057sub))
3211_0_getR_FieldAccess(EOS(STATIC_3211), java.lang.Object(o2057sub), i1414, java.lang.Object(o2057sub)) → 3227_0_getR_FieldAccess(EOS(STATIC_3227), java.lang.Object(o2057sub), i1414, java.lang.Object(o2057sub))
3226_0_getR_FieldAccess(EOS(STATIC_3226), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096))) → 3240_0_getR_FieldAccess(EOS(STATIC_3240), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)))
3240_0_getR_FieldAccess(EOS(STATIC_3240), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096))) → 3256_0_getR_NONNULL(EOS(STATIC_3256), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1414, o2096)
3256_0_getR_NONNULL(EOS(STATIC_3256), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1414, java.lang.Object(o2132sub)) → 3278_0_getR_NONNULL(EOS(STATIC_3278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1414, java.lang.Object(o2132sub))
3278_0_getR_NONNULL(EOS(STATIC_3278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1414, java.lang.Object(o2132sub)) → 3295_0_getR_Load(EOS(STATIC_3295), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1414)
3295_0_getR_Load(EOS(STATIC_3295), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1414) → 3311_0_getR_FieldAccess(EOS(STATIC_3311), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))))
3311_0_getR_FieldAccess(EOS(STATIC_3311), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub)))) → 3330_0_getR_Load(EOS(STATIC_3330), i1414, java.lang.Object(o2132sub))
3330_0_getR_Load(EOS(STATIC_3330), i1414, java.lang.Object(o2132sub)) → 3353_0_getR_ConstantStackPush(EOS(STATIC_3353), java.lang.Object(o2132sub), i1414)
3353_0_getR_ConstantStackPush(EOS(STATIC_3353), java.lang.Object(o2132sub), i1414) → 3369_0_getR_IntArithmetic(EOS(STATIC_3369), java.lang.Object(o2132sub), i1414, 1)
3369_0_getR_IntArithmetic(EOS(STATIC_3369), java.lang.Object(o2132sub), i1414, matching1) → 3394_0_getR_InvokeMethod(EOS(STATIC_3394), java.lang.Object(o2132sub), -(i1414, 1)) | &&(>(i1414, 0), =(matching1, 1))
3394_0_getR_InvokeMethod(EOS(STATIC_3394), java.lang.Object(o2132sub), i1491) → 3433_1_getR_InvokeMethod(3433_0_getR_Load(EOS(STATIC_3433), java.lang.Object(o2132sub), i1491), java.lang.Object(o2132sub), i1491)
3433_0_getR_Load(EOS(STATIC_3433), java.lang.Object(o2132sub), i1491) → 3451_0_getR_Load(EOS(STATIC_3451), java.lang.Object(o2132sub), i1491)
3451_0_getR_Load(EOS(STATIC_3451), java.lang.Object(o2132sub), i1491) → 3472_0_getR_Load(EOS(STATIC_3472), java.lang.Object(o2132sub), i1491)
3472_0_getR_Load(EOS(STATIC_3472), java.lang.Object(o2280sub), i1491) → 3499_0_getR_Load(EOS(STATIC_3499), java.lang.Object(o2280sub), i1491)
3499_0_getR_Load(EOS(STATIC_3499), java.lang.Object(o2280sub), i1491) → 3181_0_getR_Load(EOS(STATIC_3181), java.lang.Object(o2280sub), i1491)
3181_0_getR_Load(EOS(STATIC_3181), java.lang.Object(o2057sub), i1408) → 3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(o2057sub), i1408, i1408)
3227_0_getR_FieldAccess(EOS(STATIC_3227), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099))) → 3241_0_getR_FieldAccess(EOS(STATIC_3241), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)))
3241_0_getR_FieldAccess(EOS(STATIC_3241), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099))) → 3262_0_getR_NONNULL(EOS(STATIC_3262), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1414, o2099)
3262_0_getR_NONNULL(EOS(STATIC_3262), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1414, java.lang.Object(o2133sub)) → 3280_0_getR_NONNULL(EOS(STATIC_3280), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1414, java.lang.Object(o2133sub))
3280_0_getR_NONNULL(EOS(STATIC_3280), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1414, java.lang.Object(o2133sub)) → 3298_0_getR_Load(EOS(STATIC_3298), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1414)
3298_0_getR_Load(EOS(STATIC_3298), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1414) → 3314_0_getR_FieldAccess(EOS(STATIC_3314), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))))
3314_0_getR_FieldAccess(EOS(STATIC_3314), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub)))) → 3333_0_getR_Load(EOS(STATIC_3333), i1414, java.lang.Object(o2133sub))
3333_0_getR_Load(EOS(STATIC_3333), i1414, java.lang.Object(o2133sub)) → 3355_0_getR_ConstantStackPush(EOS(STATIC_3355), java.lang.Object(o2133sub), i1414)
3355_0_getR_ConstantStackPush(EOS(STATIC_3355), java.lang.Object(o2133sub), i1414) → 3371_0_getR_IntArithmetic(EOS(STATIC_3371), java.lang.Object(o2133sub), i1414, 1)
3371_0_getR_IntArithmetic(EOS(STATIC_3371), java.lang.Object(o2133sub), i1414, matching1) → 3396_0_getR_InvokeMethod(EOS(STATIC_3396), java.lang.Object(o2133sub), -(i1414, 1)) | &&(>(i1414, 0), =(matching1, 1))
3396_0_getR_InvokeMethod(EOS(STATIC_3396), java.lang.Object(o2133sub), i1492) → 3434_1_getR_InvokeMethod(3434_0_getR_Load(EOS(STATIC_3434), java.lang.Object(o2133sub), i1492), java.lang.Object(o2133sub), i1492)
3434_0_getR_Load(EOS(STATIC_3434), java.lang.Object(o2133sub), i1492) → 3453_0_getR_Load(EOS(STATIC_3453), java.lang.Object(o2133sub), i1492)
3453_0_getR_Load(EOS(STATIC_3453), java.lang.Object(o2133sub), i1492) → 3501_0_getR_Load(EOS(STATIC_3501), java.lang.Object(o2133sub), i1492)
3501_0_getR_Load(EOS(STATIC_3501), java.lang.Object(o2133sub), i1492) → 3181_0_getR_Load(EOS(STATIC_3181), java.lang.Object(o2133sub), i1492)
R rules:
3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(o2057sub), matching1, matching2) → 3196_0_getR_EQ(EOS(STATIC_3196), java.lang.Object(o2057sub), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
3196_0_getR_EQ(EOS(STATIC_3196), java.lang.Object(o2057sub), matching1, matching2) → 3203_0_getR_Load(EOS(STATIC_3203), java.lang.Object(o2057sub), 0) | &&(=(matching1, 0), =(matching2, 0))
3203_0_getR_Load(EOS(STATIC_3203), java.lang.Object(o2057sub), matching1) → 3212_0_getR_Return(EOS(STATIC_3212), java.lang.Object(o2057sub), 0, java.lang.Object(o2057sub)) | =(matching1, 0)
3256_0_getR_NONNULL(EOS(STATIC_3256), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, NULL) → 3279_0_getR_NONNULL(EOS(STATIC_3279), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, NULL)
3262_0_getR_NONNULL(EOS(STATIC_3262), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, NULL) → 3281_0_getR_NONNULL(EOS(STATIC_3281), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, NULL)
3279_0_getR_NONNULL(EOS(STATIC_3279), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, NULL) → 3296_0_getR_Load(EOS(STATIC_3296), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414)
3281_0_getR_NONNULL(EOS(STATIC_3281), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, NULL) → 3300_0_getR_Load(EOS(STATIC_3300), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414)
3296_0_getR_Load(EOS(STATIC_3296), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414) → 3312_0_getR_Return(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3300_0_getR_Load(EOS(STATIC_3300), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414) → 3316_0_getR_Return(EOS(STATIC_3316), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1414, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(EOS(STATIC_3212), java.lang.Object(o2389sub), matching1, java.lang.Object(o2389sub)), java.lang.Object(o2389sub), matching2) → 3614_0_getR_Return(EOS(STATIC_3614), java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub)) | &&(=(matching1, 0), =(matching2, 0))
3433_1_getR_InvokeMethod(3312_0_getR_Return(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583) → 3624_0_getR_Return(EOS(STATIC_3624), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3433_1_getR_InvokeMethod(3316_0_getR_Return(EOS(STATIC_3316), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590) → 3638_0_getR_Return(EOS(STATIC_3638), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3433_1_getR_InvokeMethod(3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(o2876sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2876sub))), i1825) → 3922_0_getR_Return(EOS(STATIC_3922), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2876sub))), i1825)
3433_1_getR_InvokeMethod(3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(o2885sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2885sub))), i1836) → 3935_0_getR_Return(EOS(STATIC_3935), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2885sub))), i1836)
3433_1_getR_InvokeMethod(4203_0_getR_Return(EOS(STATIC_4203)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3444sub))))), i2114) → 4262_0_getR_Return(EOS(STATIC_4262), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3444sub))))), i2114)
3433_1_getR_InvokeMethod(4206_0_getR_Return(EOS(STATIC_4206)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3461sub))))), i2128) → 4278_0_getR_Return(EOS(STATIC_4278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3461sub))))), i2128)
3434_1_getR_InvokeMethod(3212_0_getR_Return(EOS(STATIC_3212), java.lang.Object(o2413sub), matching1, java.lang.Object(o2413sub)), java.lang.Object(o2413sub), matching2) → 3640_0_getR_Return(EOS(STATIC_3640), java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub)) | &&(=(matching1, 0), =(matching2, 0))
3434_1_getR_InvokeMethod(3312_0_getR_Return(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603) → 3649_0_getR_Return(EOS(STATIC_3649), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3434_1_getR_InvokeMethod(3316_0_getR_Return(EOS(STATIC_3316), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611) → 3655_0_getR_Return(EOS(STATIC_3655), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3434_1_getR_InvokeMethod(3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(o2881sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2881sub))), i1830) → 3923_0_getR_Return(EOS(STATIC_3923), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2881sub))), i1830)
3434_1_getR_InvokeMethod(3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(o2890sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2890sub))), i1842) → 3942_0_getR_Return(EOS(STATIC_3942), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2890sub))), i1842)
3434_1_getR_InvokeMethod(4203_0_getR_Return(EOS(STATIC_4203)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3451sub))))), i2120) → 4269_0_getR_Return(EOS(STATIC_4269), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3451sub))))), i2120)
3434_1_getR_InvokeMethod(4206_0_getR_Return(EOS(STATIC_4206)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3468sub))))), i2135) → 4285_0_getR_Return(EOS(STATIC_4285), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3468sub))))), i2135)
3614_0_getR_Return(EOS(STATIC_3614), java.lang.Object(o2389sub), matching1, java.lang.Object(o2389sub), matching2, java.lang.Object(o2389sub)) → 3625_0_getR_Return(EOS(STATIC_3625), java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub)) | &&(=(matching1, 0), =(matching2, 0))
3624_0_getR_Return(EOS(STATIC_3624), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3625_0_getR_Return(EOS(STATIC_3625), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1583, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3625_0_getR_Return(EOS(STATIC_3625), java.lang.Object(o2525sub), i1650, java.lang.Object(o2525sub), i1650, java.lang.Object(o2525sub)) → 3639_0_getR_Return(EOS(STATIC_3639), java.lang.Object(o2525sub), i1650, java.lang.Object(o2525sub), i1650, java.lang.Object(o2525sub))
3638_0_getR_Return(EOS(STATIC_3638), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3639_0_getR_Return(EOS(STATIC_3639), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1590, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3639_0_getR_Return(EOS(STATIC_3639), java.lang.Object(o2539sub), i1655, java.lang.Object(o2539sub), i1655, java.lang.Object(o2539sub)) → 3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(o2539sub))
3640_0_getR_Return(EOS(STATIC_3640), java.lang.Object(o2413sub), matching1, java.lang.Object(o2413sub), matching2, java.lang.Object(o2413sub)) → 3650_0_getR_Return(EOS(STATIC_3650), java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub)) | &&(=(matching1, 0), =(matching2, 0))
3649_0_getR_Return(EOS(STATIC_3649), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3650_0_getR_Return(EOS(STATIC_3650), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1603, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3650_0_getR_Return(EOS(STATIC_3650), java.lang.Object(o2558sub), i1665, java.lang.Object(o2558sub), i1665, java.lang.Object(o2558sub)) → 3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(o2558sub))
3655_0_getR_Return(EOS(STATIC_3655), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3650_0_getR_Return(EOS(STATIC_3650), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1611, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3922_0_getR_Return(EOS(STATIC_3922), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2876sub))), i1825) → 3936_0_getR_Return(EOS(STATIC_3936), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2876sub))), i1825)
3923_0_getR_Return(EOS(STATIC_3923), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2881sub))), i1830) → 4172_0_getR_Return(EOS(STATIC_4172), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2881sub))), i1830)
3935_0_getR_Return(EOS(STATIC_3935), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2885sub))), i1836) → 3936_0_getR_Return(EOS(STATIC_3936), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2885sub))), i1836)
3936_0_getR_Return(EOS(STATIC_3936), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3002sub))), i1880) → 4155_0_getR_Return(EOS(STATIC_4155), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3002sub))), i1880)
3942_0_getR_Return(EOS(STATIC_3942), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2890sub))), i1842) → 3923_0_getR_Return(EOS(STATIC_3923), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2890sub))), i1842)
4155_0_getR_Return(EOS(STATIC_4155), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3278sub))), i2044) → 4203_0_getR_Return(EOS(STATIC_4203))
4172_0_getR_Return(EOS(STATIC_4172), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3326sub))), i2068) → 4206_0_getR_Return(EOS(STATIC_4206))
4262_0_getR_Return(EOS(STATIC_4262), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3444sub))))), i2114) → 4155_0_getR_Return(EOS(STATIC_4155), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3444sub))))), i2114)
4269_0_getR_Return(EOS(STATIC_4269), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3451sub))))), i2120) → 4172_0_getR_Return(EOS(STATIC_4172), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3451sub))))), i2120)
4278_0_getR_Return(EOS(STATIC_4278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3461sub))))), i2128) → 4155_0_getR_Return(EOS(STATIC_4155), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3461sub))))), i2128)
4285_0_getR_Return(EOS(STATIC_4285), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3468sub))))), i2135) → 4172_0_getR_Return(EOS(STATIC_4172), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3468sub))))), i2135)

Combined rules. Obtained 2 conditional rules for P and 15 conditional rules for R.

P rules:
3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1, x1) → 3433_1_getR_InvokeMethod(3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(x0), -(x1, 1), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1, x1) → 3434_1_getR_InvokeMethod(3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(x0), -(x1, 1), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
R rules:
3189_0_getR_EQ(EOS(STATIC_3189), java.lang.Object(x0), 0, 0) → 3212_0_getR_Return(EOS(STATIC_3212), java.lang.Object(x0), 0, java.lang.Object(x0))
3433_1_getR_InvokeMethod(3316_0_getR_Return(EOS(STATIC_3316), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(EOS(STATIC_3212), java.lang.Object(x0), 0, java.lang.Object(x0)), java.lang.Object(x0), 0) → 3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(x0))
3433_1_getR_InvokeMethod(3312_0_getR_Return(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3434_1_getR_InvokeMethod(3212_0_getR_Return(EOS(STATIC_3212), java.lang.Object(x0), 0, java.lang.Object(x0)), java.lang.Object(x0), 0) → 3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(x0))
3434_1_getR_InvokeMethod(3312_0_getR_Return(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3434_1_getR_InvokeMethod(3316_0_getR_Return(EOS(STATIC_3316), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3434_1_getR_InvokeMethod(3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4206_0_getR_Return(EOS(STATIC_4206))
3434_1_getR_InvokeMethod(3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4206_0_getR_Return(EOS(STATIC_4206))
3434_1_getR_InvokeMethod(4203_0_getR_Return(EOS(STATIC_4203)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4206_0_getR_Return(EOS(STATIC_4206))
3434_1_getR_InvokeMethod(4206_0_getR_Return(EOS(STATIC_4206)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4206_0_getR_Return(EOS(STATIC_4206))
3433_1_getR_InvokeMethod(4203_0_getR_Return(EOS(STATIC_4203)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4203_0_getR_Return(EOS(STATIC_4203))
3433_1_getR_InvokeMethod(4206_0_getR_Return(EOS(STATIC_4206)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4203_0_getR_Return(EOS(STATIC_4203))
3433_1_getR_InvokeMethod(3676_0_getR_Return(EOS(STATIC_3676), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4203_0_getR_Return(EOS(STATIC_4203))
3433_1_getR_InvokeMethod(3679_0_getR_Return(EOS(STATIC_3679), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4203_0_getR_Return(EOS(STATIC_4203))

Filtered ground terms:

3189_0_getR_EQ(x1, x2, x3, x4) → 3189_0_getR_EQ(x2, x3, x4)
Cond_3189_0_getR_EQ1(x1, x2, x3, x4, x5) → Cond_3189_0_getR_EQ1(x1, x3, x4, x5)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
Cond_3189_0_getR_EQ(x1, x2, x3, x4, x5) → Cond_3189_0_getR_EQ(x1, x3, x4, x5)
4203_0_getR_Return(x1) → 4203_0_getR_Return
3679_0_getR_Return(x1, x2) → 3679_0_getR_Return(x2)
3676_0_getR_Return(x1, x2) → 3676_0_getR_Return(x2)
4206_0_getR_Return(x1) → 4206_0_getR_Return
3316_0_getR_Return(x1, x2, x3, x4) → 3316_0_getR_Return(x3)
3312_0_getR_Return(x1, x2, x3, x4) → 3312_0_getR_Return(x3)
3212_0_getR_Return(x1, x2, x3, x4) → 3212_0_getR_Return(x2, x4)

Filtered duplicate args:

3189_0_getR_EQ(x1, x2, x3) → 3189_0_getR_EQ(x1, x3)
Cond_3189_0_getR_EQ(x1, x2, x3, x4) → Cond_3189_0_getR_EQ(x1, x2, x4)
Cond_3189_0_getR_EQ1(x1, x2, x3, x4) → Cond_3189_0_getR_EQ1(x1, x2, x4)
3212_0_getR_Return(x1, x2) → 3212_0_getR_Return(x2)

Combined rules. Obtained 2 conditional rules for P and 15 conditional rules for R.

P rules:
3189_0_getR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3433_1_getR_InvokeMethod(3189_0_getR_EQ(java.lang.Object(x0), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
3189_0_getR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3434_1_getR_InvokeMethod(3189_0_getR_EQ(java.lang.Object(x0), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
R rules:
3189_0_getR_EQ(java.lang.Object(x0), 0) → 3212_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3676_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3676_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3312_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3676_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3434_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3679_0_getR_Return(java.lang.Object(x0))
3434_1_getR_InvokeMethod(3312_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3679_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3434_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3679_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3434_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4206_0_getR_Return
3434_1_getR_InvokeMethod(3679_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4206_0_getR_Return
3434_1_getR_InvokeMethod(4203_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4206_0_getR_Return
3434_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4206_0_getR_Return
3433_1_getR_InvokeMethod(4203_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4203_0_getR_Return
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4203_0_getR_Return
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4203_0_getR_Return
3433_1_getR_InvokeMethod(3679_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4203_0_getR_Return

Performed bisimulation on rules. Used the following equivalence classes: {[3676_0_getR_Return_1, 3679_0_getR_Return_1]=3676_0_getR_Return_1, [3316_0_getR_Return_1, 3312_0_getR_Return_1]=3316_0_getR_Return_1, [3433_1_getR_InvokeMethod_3, 3434_1_getR_InvokeMethod_3]=3433_1_getR_InvokeMethod_3, [Cond_3189_0_getR_EQ_3, Cond_3189_0_getR_EQ1_3]=Cond_3189_0_getR_EQ_3, [4206_0_getR_Return, 4203_0_getR_Return]=4206_0_getR_Return}

Finished conversion. Obtained 2 rules for P and 5 rules for R. System has predefined symbols.

P rules:
3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → COND_3189_0_GETR_EQ(>(x1, 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3189_0_GETR_EQ(java.lang.Object(x0), -(x1, 1))
R rules:
3189_0_getR_EQ(java.lang.Object(x0), 0) → 3212_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3676_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3676_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4206_0_getR_Return
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4206_0_getR_Return

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3189_0_getR_EQ(java.lang.Object(x0), 0) → 3212_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3676_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3676_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4206_0_getR_Return
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4206_0_getR_Return

The integer pair graph contains the following rules and edges:
(0): 3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3189_0_GETR_EQ(x1[0] > 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])
(1): COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3189_0_GETR_EQ(java.lang.Object(x0[1]), x1[1] - 1)

(0) -> (1), if (x1[0] > 0 ∧java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))) →^* java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1])))∧x1[0] →^* x1[1])

(1) -> (0), if (java.lang.Object(x0[1]) →^* java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))∧x1[1] - 1 →^* x1[0])

The set Q consists of the following terms:
3189_0_getR_EQ(java.lang.Object(x0), 0)
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0)
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0)
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1)

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@1b32991a Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → COND_3189_0_GETR_EQ(>(x1, 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) the following chains were created:

We consider the chain 3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]), COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1)) which results in the following constraint:
(1)    (>(x1[0], 0)=TRUE∧java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))=java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1])))∧x1[0]=x1[1] ⇒ 3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥NonInfC∧3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])∧(U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (>(x1[0], 0)=TRUE ⇒ 3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥NonInfC∧3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])∧(U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17 + (2)bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

For Pair COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3189_0_GETR_EQ(java.lang.Object(x0), -(x1, 1)) the following chains were created:

We consider the chain COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1)) which results in the following constraint:
(7)    (COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1])≥NonInfC∧COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1])≥3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))∧(U^Increasing(3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧0 = 0∧[2 + (-1)bso_20] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → COND_3189_0_GETR_EQ(>(x1, 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
- (x1[0] ≥ 0 ⇒ (U^Increasing(COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17 + (2)bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)
COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3189_0_GETR_EQ(java.lang.Object(x0), -(x1, 1))
- ((U^Increasing(3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧0 = 0∧[2 + (-1)bso_20] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(3189_0_getR_EQ(x₁, x₂)) = [-1]
POL(java.lang.Object(x₁)) = [-1]
POL(0) = 0
POL(3212_0_getR_Return(x₁)) = [-1]
POL(3433_1_getR_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(3316_0_getR_Return(x₁)) = [-1]
POL(DoublyLinkedList.DoublyLinkedList(x₁)) = [-1]
POL(NULL) = [-1]
POL(3676_0_getR_Return(x₁)) = [-1]
POL(4206_0_getR_Return) = [-1]
POL(3189_0_GETR_EQ(x₁, x₂)) = [2]x₂
POL(COND_3189_0_GETR_EQ(x₁, x₂, x₃)) = [2]x₃
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(1) = [1]

The following pairs are in P_>:

COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3189_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))

The following pairs are in P_bound:

3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])

The following pairs are in P_≥:

3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3189_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])

There are no usable rules.

(9) Complex Obligation (AND)

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3189_0_getR_EQ(java.lang.Object(x0), 0) → 3212_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3676_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3676_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4206_0_getR_Return
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4206_0_getR_Return

The integer pair graph contains the following rules and edges:
(0): 3189_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3189_0_GETR_EQ(x1[0] > 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])

The set Q consists of the following terms:
3189_0_getR_EQ(java.lang.Object(x0), 0)
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0)
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0)
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1)

(11) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(12) TRUE

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3189_0_getR_EQ(java.lang.Object(x0), 0) → 3212_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3676_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3676_0_getR_Return(java.lang.Object(x0))
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4206_0_getR_Return
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4206_0_getR_Return

The integer pair graph contains the following rules and edges:
(1): COND_3189_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3189_0_GETR_EQ(java.lang.Object(x0[1]), x1[1] - 1)

The set Q consists of the following terms:
3189_0_getR_EQ(java.lang.Object(x0), 0)
3433_1_getR_InvokeMethod(3316_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0)
3433_1_getR_InvokeMethod(3212_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0)
3433_1_getR_InvokeMethod(3676_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
3433_1_getR_InvokeMethod(4206_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1)

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(15) TRUE

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DoublyLinkedList.DoublyLinkedList.getFirst()LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods: DoublyLinkedList.DoublyLinkedList.getFirst()LDoublyLinkedList/DoublyLinkedList;
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 24 rules for P and 35 rules for R.

P rules:
3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(o2063sub), java.lang.Object(o2063sub)) → 3200_0_getFirst_FieldAccess(EOS(STATIC_3200), java.lang.Object(o2063sub), java.lang.Object(o2063sub))
3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(o2063sub), java.lang.Object(o2063sub)) → 3201_0_getFirst_FieldAccess(EOS(STATIC_3201), java.lang.Object(o2063sub), java.lang.Object(o2063sub))
3200_0_getFirst_FieldAccess(EOS(STATIC_3200), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071))) → 3208_0_getFirst_FieldAccess(EOS(STATIC_3208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)))
3208_0_getFirst_FieldAccess(EOS(STATIC_3208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071))) → 3219_0_getFirst_NONNULL(EOS(STATIC_3219), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), o2071)
3219_0_getFirst_NONNULL(EOS(STATIC_3219), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))), java.lang.Object(o2092sub)) → 3235_0_getFirst_NONNULL(EOS(STATIC_3235), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))), java.lang.Object(o2092sub))
3235_0_getFirst_NONNULL(EOS(STATIC_3235), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))), java.lang.Object(o2092sub)) → 3249_0_getFirst_Load(EOS(STATIC_3249), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))))
3249_0_getFirst_Load(EOS(STATIC_3249), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub)))) → 3270_0_getFirst_FieldAccess(EOS(STATIC_3270), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))))
3270_0_getFirst_FieldAccess(EOS(STATIC_3270), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub)))) → 3289_0_getFirst_InvokeMethod(EOS(STATIC_3289), java.lang.Object(o2092sub))
3289_0_getFirst_InvokeMethod(EOS(STATIC_3289), java.lang.Object(o2092sub)) → 3308_1_getFirst_InvokeMethod(3308_0_getFirst_Load(EOS(STATIC_3308), java.lang.Object(o2092sub)), java.lang.Object(o2092sub))
3308_0_getFirst_Load(EOS(STATIC_3308), java.lang.Object(o2092sub)) → 3327_0_getFirst_Load(EOS(STATIC_3327), java.lang.Object(o2092sub))
3327_0_getFirst_Load(EOS(STATIC_3327), java.lang.Object(o2092sub)) → 3352_0_getFirst_Load(EOS(STATIC_3352), java.lang.Object(o2092sub))
3352_0_getFirst_Load(EOS(STATIC_3352), java.lang.Object(o2175sub)) → 3364_0_getFirst_Load(EOS(STATIC_3364), java.lang.Object(o2175sub))
3364_0_getFirst_Load(EOS(STATIC_3364), java.lang.Object(o2175sub)) → 3187_0_getFirst_Load(EOS(STATIC_3187), java.lang.Object(o2175sub))
3187_0_getFirst_Load(EOS(STATIC_3187), java.lang.Object(o2063sub)) → 3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(o2063sub), java.lang.Object(o2063sub))
3201_0_getFirst_FieldAccess(EOS(STATIC_3201), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074))) → 3209_0_getFirst_FieldAccess(EOS(STATIC_3209), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)))
3209_0_getFirst_FieldAccess(EOS(STATIC_3209), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074))) → 3224_0_getFirst_NONNULL(EOS(STATIC_3224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), o2074)
3224_0_getFirst_NONNULL(EOS(STATIC_3224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))), java.lang.Object(o2093sub)) → 3237_0_getFirst_NONNULL(EOS(STATIC_3237), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))), java.lang.Object(o2093sub))
3237_0_getFirst_NONNULL(EOS(STATIC_3237), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))), java.lang.Object(o2093sub)) → 3252_0_getFirst_Load(EOS(STATIC_3252), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))))
3252_0_getFirst_Load(EOS(STATIC_3252), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub)))) → 3274_0_getFirst_FieldAccess(EOS(STATIC_3274), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))))
3274_0_getFirst_FieldAccess(EOS(STATIC_3274), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub)))) → 3292_0_getFirst_InvokeMethod(EOS(STATIC_3292), java.lang.Object(o2093sub))
3292_0_getFirst_InvokeMethod(EOS(STATIC_3292), java.lang.Object(o2093sub)) → 3309_1_getFirst_InvokeMethod(3309_0_getFirst_Load(EOS(STATIC_3309), java.lang.Object(o2093sub)), java.lang.Object(o2093sub))
3309_0_getFirst_Load(EOS(STATIC_3309), java.lang.Object(o2093sub)) → 3329_0_getFirst_Load(EOS(STATIC_3329), java.lang.Object(o2093sub))
3329_0_getFirst_Load(EOS(STATIC_3329), java.lang.Object(o2093sub)) → 3367_0_getFirst_Load(EOS(STATIC_3367), java.lang.Object(o2093sub))
3367_0_getFirst_Load(EOS(STATIC_3367), java.lang.Object(o2093sub)) → 3187_0_getFirst_Load(EOS(STATIC_3187), java.lang.Object(o2093sub))
R rules:
3219_0_getFirst_NONNULL(EOS(STATIC_3219), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3236_0_getFirst_NONNULL(EOS(STATIC_3236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3224_0_getFirst_NONNULL(EOS(STATIC_3224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3238_0_getFirst_NONNULL(EOS(STATIC_3238), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3236_0_getFirst_NONNULL(EOS(STATIC_3236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3250_0_getFirst_Load(EOS(STATIC_3250), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3238_0_getFirst_NONNULL(EOS(STATIC_3238), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3254_0_getFirst_Load(EOS(STATIC_3254), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3250_0_getFirst_Load(EOS(STATIC_3250), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3272_0_getFirst_Return(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3254_0_getFirst_Load(EOS(STATIC_3254), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3276_0_getFirst_Return(EOS(STATIC_3276), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3272_0_getFirst_Return(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3407_0_getFirst_Return(EOS(STATIC_3407), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3276_0_getFirst_Return(EOS(STATIC_3276), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3421_0_getFirst_Return(EOS(STATIC_3421), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3522_0_getFirst_Return(EOS(STATIC_3522), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3541_0_getFirst_Return(EOS(STATIC_3541), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(o2741sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103))))))) → 4038_0_getFirst_Return(EOS(STATIC_4038), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103)))))), java.lang.Object(o2741sub))
3308_1_getFirst_InvokeMethod(3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(o2818sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3128))))))) → 4082_0_getFirst_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3128)))))), java.lang.Object(o2818sub))
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3424_0_getFirst_Return(EOS(STATIC_3424), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3276_0_getFirst_Return(EOS(STATIC_3276), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3431_0_getFirst_Return(EOS(STATIC_3431), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3523_0_getFirst_Return(EOS(STATIC_3523), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3551_0_getFirst_Return(EOS(STATIC_3551), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(o2741sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112))))))) → 4050_0_getFirst_Return(EOS(STATIC_4050), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112)))))), java.lang.Object(o2741sub))
3309_1_getFirst_InvokeMethod(3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(o2818sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3137))))))) → 4095_0_getFirst_Return(EOS(STATIC_4095), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3137)))))), java.lang.Object(o2818sub))
3407_0_getFirst_Return(EOS(STATIC_3407), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3422_0_getFirst_Return(EOS(STATIC_3422), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3421_0_getFirst_Return(EOS(STATIC_3421), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3422_0_getFirst_Return(EOS(STATIC_3422), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3422_0_getFirst_Return(EOS(STATIC_3422), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3424_0_getFirst_Return(EOS(STATIC_3424), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3431_0_getFirst_Return(EOS(STATIC_3431), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3424_0_getFirst_Return(EOS(STATIC_3424), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3522_0_getFirst_Return(EOS(STATIC_3522), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3542_0_getFirst_Return(EOS(STATIC_3542), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3523_0_getFirst_Return(EOS(STATIC_3523), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3795_0_getFirst_Return(EOS(STATIC_3795), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3541_0_getFirst_Return(EOS(STATIC_3541), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3542_0_getFirst_Return(EOS(STATIC_3542), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3542_0_getFirst_Return(EOS(STATIC_3542), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3762_0_getFirst_Return(EOS(STATIC_3762), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3551_0_getFirst_Return(EOS(STATIC_3551), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3523_0_getFirst_Return(EOS(STATIC_3523), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3762_0_getFirst_Return(EOS(STATIC_3762), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2673)))), java.lang.Object(o2676sub)) → 3862_0_getFirst_Return(EOS(STATIC_3862), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2673)))), java.lang.Object(o2676sub))
3795_0_getFirst_Return(EOS(STATIC_3795), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2738)))), java.lang.Object(o2741sub)) → 3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(o2741sub))
3862_0_getFirst_Return(EOS(STATIC_3862), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2815)))), java.lang.Object(o2818sub)) → 3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(o2818sub))
4038_0_getFirst_Return(EOS(STATIC_4038), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103)))))), java.lang.Object(o2741sub)) → 3862_0_getFirst_Return(EOS(STATIC_3862), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103)))))), java.lang.Object(o2741sub))
4050_0_getFirst_Return(EOS(STATIC_4050), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112)))))), java.lang.Object(o2741sub)) → 3795_0_getFirst_Return(EOS(STATIC_3795), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112)))))), java.lang.Object(o2741sub))
4082_0_getFirst_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3128)))))), java.lang.Object(o2818sub)) → 3862_0_getFirst_Return(EOS(STATIC_3862), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3128)))))), java.lang.Object(o2818sub))
4095_0_getFirst_Return(EOS(STATIC_4095), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3137)))))), java.lang.Object(o2818sub)) → 3795_0_getFirst_Return(EOS(STATIC_3795), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3137)))))), java.lang.Object(o2818sub))

Combined rules. Obtained 2 conditional rules for P and 12 conditional rules for R.

P rules:
3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3308_1_getFirst_InvokeMethod(3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3309_1_getFirst_InvokeMethod(3194_0_getFirst_FieldAccess(EOS(STATIC_3194), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3276_0_getFirst_Return(EOS(STATIC_3276), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3272_0_getFirst_Return(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3276_0_getFirst_Return(EOS(STATIC_3276), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(x0))
3309_1_getFirst_InvokeMethod(3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(x0))
3308_1_getFirst_InvokeMethod(3910_0_getFirst_Return(EOS(STATIC_3910), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(x0))
3308_1_getFirst_InvokeMethod(3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(x0))
3308_1_getFirst_InvokeMethod(3445_0_getFirst_Return(EOS(STATIC_3445), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3308_1_getFirst_InvokeMethod(3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))

Filtered ground terms:

3194_0_getFirst_FieldAccess(x1, x2, x3) → 3194_0_getFirst_FieldAccess(x2, x3)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
3921_0_getFirst_Return(x1, x2) → 3921_0_getFirst_Return(x2)
3449_0_getFirst_Return(x1, x2) → 3449_0_getFirst_Return
3445_0_getFirst_Return(x1, x2) → 3445_0_getFirst_Return
3910_0_getFirst_Return(x1, x2) → 3910_0_getFirst_Return(x2)
3276_0_getFirst_Return(x1, x2, x3) → 3276_0_getFirst_Return
3272_0_getFirst_Return(x1, x2, x3) → 3272_0_getFirst_Return

Filtered duplicate args:

3194_0_getFirst_FieldAccess(x1, x2) → 3194_0_getFirst_FieldAccess(x2)

Combined rules. Obtained 2 conditional rules for P and 12 conditional rules for R.

P rules:
3194_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3308_1_getFirst_InvokeMethod(3194_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
3194_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3309_1_getFirst_InvokeMethod(3194_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3449_0_getFirst_Return
3309_1_getFirst_InvokeMethod(3276_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3449_0_getFirst_Return
3308_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3445_0_getFirst_Return
3308_1_getFirst_InvokeMethod(3276_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3445_0_getFirst_Return
3309_1_getFirst_InvokeMethod(3445_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3910_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3449_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3910_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3910_0_getFirst_Return(java.lang.Object(x0))
3309_1_getFirst_InvokeMethod(3921_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3910_0_getFirst_Return(java.lang.Object(x0))
3308_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3921_0_getFirst_Return(java.lang.Object(x0))
3308_1_getFirst_InvokeMethod(3921_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3921_0_getFirst_Return(java.lang.Object(x0))
3308_1_getFirst_InvokeMethod(3445_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3921_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3308_1_getFirst_InvokeMethod(3449_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3921_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))

Performed bisimulation on rules. Used the following equivalence classes: {[3309_1_getFirst_InvokeMethod_2, 3308_1_getFirst_InvokeMethod_2]=3309_1_getFirst_InvokeMethod_2, [3272_0_getFirst_Return, 3449_0_getFirst_Return, 3276_0_getFirst_Return, 3445_0_getFirst_Return]=3272_0_getFirst_Return, [3910_0_getFirst_Return_1, 3921_0_getFirst_Return_1]=3910_0_getFirst_Return_1}

Finished conversion. Obtained 1 rules for P and 3 rules for R. System has no predefined symbols.

P rules:
3194_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(x0))
R rules:
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3272_0_getFirst_Return
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3910_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3910_0_getFirst_Return(java.lang.Object(x0))

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3272_0_getFirst_Return
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3910_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3910_0_getFirst_Return(java.lang.Object(x0))

The integer pair graph contains the following rules and edges:
(0): 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

(0) -> (0), if (java.lang.Object(x0[0]) →^* java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]'))))

The set Q consists of the following terms:
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

(19) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3194_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

The TRS R consists of the following rules:

3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3272_0_getFirst_Return
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3910_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3910_0_getFirst_Return(java.lang.Object(x0))

The set Q consists of the following terms:

3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

We have to consider all minimal (P,Q,R)-chains.

(21) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3194_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

R is empty.
The set Q consists of the following terms:

3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

We have to consider all minimal (P,Q,R)-chains.

(23) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3309_1_getFirst_InvokeMethod(3272_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3309_1_getFirst_InvokeMethod(3910_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3194_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

3194_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3194_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))
The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DoublyLinkedList.DoublyLinkedList.createList()LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(28) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 94 rules for P and 0 rules for R.

P rules:
3040_0_createList_Load(EOS(STATIC_3040(i1339)), i190, o1932, i1340, i1340) → 3056_0_createList_GE(EOS(STATIC_3056(i1339)), i190, o1932, i1340, i1340, i190)
3056_0_createList_GE(EOS(STATIC_3056(i1339)), i190, o1932, i1340, i1340, i190) → 3075_0_createList_GE(EOS(STATIC_3075(i1339)), i190, o1932, i1340, i1340, i190)
3075_0_createList_GE(EOS(STATIC_3075(i1339)), i190, o1932, i1340, i1340, i190) → 3092_0_createList_Load(EOS(STATIC_3092(i1339)), i190, o1932, i1340) | <(i1340, i190)
3092_0_createList_Load(EOS(STATIC_3092(i1339)), i190, o1932, i1340) → 3113_0_createList_Store(EOS(STATIC_3113(i1339)), i190, i1340, o1932)
3113_0_createList_Store(EOS(STATIC_3113(i1339)), i190, i1340, o1932) → 3126_0_createList_New(EOS(STATIC_3126(i1339)), i190, i1340, o1932)
3126_0_createList_New(EOS(STATIC_3126(i1339)), i190, i1340, o1932) → 3137_0_createList_Duplicate(EOS(STATIC_3137(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3137_0_createList_Duplicate(EOS(STATIC_3137(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3154_0_createList_InvokeMethod(EOS(STATIC_3154(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3154_0_createList_InvokeMethod(EOS(STATIC_3154(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3163_0_random_FieldAccess(EOS(STATIC_3163(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3163_0_random_FieldAccess(EOS(STATIC_3163(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3184_0_random_ArrayLength(EOS(STATIC_3184(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)))
3184_0_random_ArrayLength(EOS(STATIC_3184(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188))) → 3192_0_random_FieldAccess(EOS(STATIC_3192(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188) | >=(i188, 0)
3192_0_random_FieldAccess(EOS(STATIC_3192(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188) → 3198_0_random_GT(EOS(STATIC_3198(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339)
3198_0_random_GT(EOS(STATIC_3198(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3206_0_random_GT(EOS(STATIC_3206(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339)
3198_0_random_GT(EOS(STATIC_3198(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3207_0_random_GT(EOS(STATIC_3207(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339)
3206_0_random_GT(EOS(STATIC_3206(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3215_0_random_FieldAccess(EOS(STATIC_3215(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | >(i188, i1339)
3215_0_random_FieldAccess(EOS(STATIC_3215(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3231_0_random_FieldAccess(EOS(STATIC_3231(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)))
3231_0_random_FieldAccess(EOS(STATIC_3231(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188))) → 3246_0_random_ArrayAccess(EOS(STATIC_3246(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339)
3246_0_random_ArrayAccess(EOS(STATIC_3246(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339) → 3266_0_random_ArrayAccess(EOS(STATIC_3266(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339)
3266_0_random_ArrayAccess(EOS(STATIC_3266(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339) → 3286_0_random_Store(EOS(STATIC_3286(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) | <(i1339, i188)
3286_0_random_Store(EOS(STATIC_3286(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) → 3305_0_random_FieldAccess(EOS(STATIC_3305(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134)
3305_0_random_FieldAccess(EOS(STATIC_3305(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) → 3323_0_random_ConstantStackPush(EOS(STATIC_3323(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339)
3323_0_random_ConstantStackPush(EOS(STATIC_3323(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339) → 3343_0_random_IntArithmetic(EOS(STATIC_3343(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339, 1)
3343_0_random_IntArithmetic(EOS(STATIC_3343(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339, matching1) → 3362_0_random_FieldAccess(EOS(STATIC_3362(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, +(i1339, 1)) | &&(>=(i1339, 0), =(matching1, 1))
3362_0_random_FieldAccess(EOS(STATIC_3362(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1462) → 3376_0_random_Load(EOS(STATIC_3376(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134)
3376_0_random_Load(EOS(STATIC_3376(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) → 3403_0_random_NONNULL(EOS(STATIC_3403(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, o2134)
3403_0_random_NONNULL(EOS(STATIC_3403(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub), java.lang.Object(o2270sub)) → 3441_0_random_NONNULL(EOS(STATIC_3441(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub), java.lang.Object(o2270sub))
3403_0_random_NONNULL(EOS(STATIC_3403(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3442_0_random_NONNULL(EOS(STATIC_3442(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL)
3441_0_random_NONNULL(EOS(STATIC_3441(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub), java.lang.Object(o2270sub)) → 3457_0_random_Load(EOS(STATIC_3457(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub))
3457_0_random_Load(EOS(STATIC_3457(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub)) → 3482_0_random_InvokeMethod(EOS(STATIC_3482(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub))
3482_0_random_InvokeMethod(EOS(STATIC_3482(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub)) → 3518_0_length_Load(EOS(STATIC_3518(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub), java.lang.Object(o2270sub))
3518_0_length_Load(EOS(STATIC_3518(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub), java.lang.Object(o2270sub)) → 3668_0_length_FieldAccess(EOS(STATIC_3668(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2270sub), java.lang.Object(o2270sub))
3668_0_length_FieldAccess(EOS(STATIC_3668(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), java.lang.Object(java.lang.String(o2607sub, i1698))) → 3689_0_length_FieldAccess(EOS(STATIC_3689(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), java.lang.Object(java.lang.String(o2607sub, i1698))) | &&(>=(i1698, 0), >=(i1699, 0))
3689_0_length_FieldAccess(EOS(STATIC_3689(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), java.lang.Object(java.lang.String(o2607sub, i1698))) → 3719_0_length_Return(EOS(STATIC_3719(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), i1698)
3719_0_length_Return(EOS(STATIC_3719(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), i1698) → 3894_0_random_Return(EOS(STATIC_3894(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
3894_0_random_Return(EOS(STATIC_3894(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 3949_0_createList_InvokeMethod(EOS(STATIC_3949(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
3949_0_createList_InvokeMethod(EOS(STATIC_3949(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 3975_0_<init>_Load(EOS(STATIC_3975(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
3975_0_<init>_Load(EOS(STATIC_3975(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4127_0_<init>_InvokeMethod(EOS(STATIC_4127(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4127_0_<init>_InvokeMethod(EOS(STATIC_4127(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4198_0_<init>_Load(EOS(STATIC_4198(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4198_0_<init>_Load(EOS(STATIC_4198(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4216_0_<init>_Load(EOS(STATIC_4216(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4216_0_<init>_Load(EOS(STATIC_4216(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4231_0_<init>_FieldAccess(EOS(STATIC_4231(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4231_0_<init>_FieldAccess(EOS(STATIC_4231(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4253_0_<init>_Return(EOS(STATIC_4253(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4253_0_<init>_Return(EOS(STATIC_4253(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4293_0_createList_Store(EOS(STATIC_4293(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4293_0_createList_Store(EOS(STATIC_4293(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4305_0_createList_Load(EOS(STATIC_4305(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
4305_0_createList_Load(EOS(STATIC_4305(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 4318_0_createList_Load(EOS(STATIC_4318(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4318_0_createList_Load(EOS(STATIC_4318(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4335_0_createList_FieldAccess(EOS(STATIC_4335(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932)
4335_0_createList_FieldAccess(EOS(STATIC_4335(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932) → 4353_0_createList_Load(EOS(STATIC_4353(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
4353_0_createList_Load(EOS(STATIC_4353(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 4373_0_createList_NULL(EOS(STATIC_4373(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, o1932)
4373_0_createList_NULL(EOS(STATIC_4373(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(o3666sub)) → 4421_0_createList_NULL(EOS(STATIC_4421(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(o3666sub))
4373_0_createList_NULL(EOS(STATIC_4373(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 4422_0_createList_NULL(EOS(STATIC_4422(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL)
4421_0_createList_NULL(EOS(STATIC_4421(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(o3666sub)) → 4438_0_createList_Load(EOS(STATIC_4438(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub))
4438_0_createList_Load(EOS(STATIC_4438(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub)) → 4449_0_createList_Load(EOS(STATIC_4449(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub))
4449_0_createList_Load(EOS(STATIC_4449(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub)) → 4457_0_createList_FieldAccess(EOS(STATIC_4457(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4457_0_createList_FieldAccess(EOS(STATIC_4457(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4464_0_createList_FieldAccess(EOS(STATIC_4464(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4464_0_createList_FieldAccess(EOS(STATIC_4464(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4471_0_createList_Inc(EOS(STATIC_4471(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
4471_0_createList_Inc(EOS(STATIC_4471(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 4481_0_createList_JMP(EOS(STATIC_4481(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
4481_0_createList_JMP(EOS(STATIC_4481(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2277) → 4503_0_createList_Load(EOS(STATIC_4503(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2277)
4503_0_createList_Load(EOS(STATIC_4503(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2277) → 3027_0_createList_Load(EOS(STATIC_3027(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2277)
3027_0_createList_Load(EOS(STATIC_3027(i1339)), i190, o1932, i1340) → 3040_0_createList_Load(EOS(STATIC_3040(i1339)), i190, o1932, i1340, i1340)
4422_0_createList_NULL(EOS(STATIC_4422(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 4440_0_createList_Inc(EOS(STATIC_4440(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
4440_0_createList_Inc(EOS(STATIC_4440(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 4451_0_createList_JMP(EOS(STATIC_4451(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
4451_0_createList_JMP(EOS(STATIC_4451(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264) → 4458_0_createList_Load(EOS(STATIC_4458(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264)
4458_0_createList_Load(EOS(STATIC_4458(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264) → 3027_0_createList_Load(EOS(STATIC_3027(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264)
3442_0_random_NONNULL(EOS(STATIC_3442(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3459_0_random_ConstantStackPush(EOS(STATIC_3459(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL)
3459_0_random_ConstantStackPush(EOS(STATIC_3459(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL) → 3484_0_random_Return(EOS(STATIC_3484(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, 0)
3484_0_random_Return(EOS(STATIC_3484(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, matching1) → 3519_0_createList_InvokeMethod(EOS(STATIC_3519(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3519_0_createList_InvokeMethod(EOS(STATIC_3519(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3949_0_createList_InvokeMethod(EOS(STATIC_3949(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3207_0_random_GT(EOS(STATIC_3207(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3217_0_random_ConstantStackPush(EOS(STATIC_3217(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | <=(i188, i1339)
3217_0_random_ConstantStackPush(EOS(STATIC_3217(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3233_0_random_Return(EOS(STATIC_3233(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0)
3233_0_random_Return(EOS(STATIC_3233(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3247_0_createList_InvokeMethod(EOS(STATIC_3247(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3247_0_createList_InvokeMethod(EOS(STATIC_3247(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3269_0_<init>_Load(EOS(STATIC_3269(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3269_0_<init>_Load(EOS(STATIC_3269(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3306_0_<init>_InvokeMethod(EOS(STATIC_3306(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3306_0_<init>_InvokeMethod(EOS(STATIC_3306(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3326_0_<init>_Load(EOS(STATIC_3326(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3326_0_<init>_Load(EOS(STATIC_3326(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3346_0_<init>_Load(EOS(STATIC_3346(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3346_0_<init>_Load(EOS(STATIC_3346(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3363_0_<init>_FieldAccess(EOS(STATIC_3363(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3363_0_<init>_FieldAccess(EOS(STATIC_3363(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3378_0_<init>_Return(EOS(STATIC_3378(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3378_0_<init>_Return(EOS(STATIC_3378(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3406_0_createList_Store(EOS(STATIC_3406(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | =(matching1, 0)
3406_0_createList_Store(EOS(STATIC_3406(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3444_0_createList_Load(EOS(STATIC_3444(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
3444_0_createList_Load(EOS(STATIC_3444(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 3462_0_createList_Load(EOS(STATIC_3462(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3462_0_createList_Load(EOS(STATIC_3462(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3487_0_createList_FieldAccess(EOS(STATIC_3487(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932)
3487_0_createList_FieldAccess(EOS(STATIC_3487(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932) → 3521_0_createList_Load(EOS(STATIC_3521(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
3521_0_createList_Load(EOS(STATIC_3521(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 3597_0_createList_NULL(EOS(STATIC_3597(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, o1932)
3597_0_createList_NULL(EOS(STATIC_3597(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(o2591sub)) → 3670_0_createList_NULL(EOS(STATIC_3670(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(o2591sub))
3597_0_createList_NULL(EOS(STATIC_3597(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 3671_0_createList_NULL(EOS(STATIC_3671(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL)
3670_0_createList_NULL(EOS(STATIC_3670(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(o2591sub)) → 3692_0_createList_Load(EOS(STATIC_3692(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub))
3692_0_createList_Load(EOS(STATIC_3692(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub)) → 3723_0_createList_Load(EOS(STATIC_3723(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub))
3723_0_createList_Load(EOS(STATIC_3723(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub)) → 3898_0_createList_FieldAccess(EOS(STATIC_3898(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3898_0_createList_FieldAccess(EOS(STATIC_3898(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3952_0_createList_FieldAccess(EOS(STATIC_3952(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3952_0_createList_FieldAccess(EOS(STATIC_3952(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3984_0_createList_Inc(EOS(STATIC_3984(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
3984_0_createList_Inc(EOS(STATIC_3984(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 4024_0_createList_JMP(EOS(STATIC_4024(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
4024_0_createList_JMP(EOS(STATIC_4024(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975) → 4133_0_createList_Load(EOS(STATIC_4133(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975)
4133_0_createList_Load(EOS(STATIC_4133(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975) → 3027_0_createList_Load(EOS(STATIC_3027(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975)
3671_0_createList_NULL(EOS(STATIC_3671(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 3693_0_createList_Inc(EOS(STATIC_3693(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
3693_0_createList_Inc(EOS(STATIC_3693(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 3724_0_createList_JMP(EOS(STATIC_3724(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
3724_0_createList_JMP(EOS(STATIC_3724(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1739) → 3900_0_createList_Load(EOS(STATIC_3900(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1739)
3900_0_createList_Load(EOS(STATIC_3900(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1739) → 3027_0_createList_Load(EOS(STATIC_3027(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1739)
R rules:

Combined rules. Obtained 5 conditional rules for P and 0 conditional rules for R.

P rules:
3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, x2, x3, x3) → 4373_0_createList_NULL(EOS(STATIC_4373(+(x0, 1))), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x3, x2, x2) | &&(<(x3, x1), >(+(x0, 1), 0))
4373_0_createList_NULL(EOS(STATIC_4373(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
4373_0_createList_NULL(EOS(STATIC_4373(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, NULL, NULL) → 3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, x2) → 3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, NULL, x2, x2) → 3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
R rules:

Filtered ground terms:

DoublyLinkedList.DoublyLinkedList(x1) → DoublyLinkedList.DoublyLinkedList
java.lang.Object(x1) → java.lang.Object
Cond_3040_0_createList_Load2(x1, x2, x3, x4, x5, x6) → Cond_3040_0_createList_Load2(x1, x2, x3, x5, x6)
Cond_3040_0_createList_Load1(x1, x2, x3, x4, x5, x6) → Cond_3040_0_createList_Load1(x1, x2, x3, x5, x6)
4373_0_createList_NULL(x1, x2, x3, x4, x5, x6) → 4373_0_createList_NULL(x1, x2, x4, x5, x6)

Filtered duplicate args:

3040_0_createList_Load(x1, x2, x3, x4, x5) → 3040_0_createList_Load(x1, x2, x3, x5)
Cond_3040_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_3040_0_createList_Load(x1, x2, x3, x4, x6)
4373_0_createList_NULL(x1, x2, x3, x4, x5) → 4373_0_createList_NULL(x1, x2, x3, x5)
Cond_3040_0_createList_Load1(x1, x2, x3, x4, x5) → Cond_3040_0_createList_Load1(x1, x2, x3, x5)
Cond_3040_0_createList_Load2(x1, x2, x3, x4, x5) → Cond_3040_0_createList_Load2(x1, x2, x3, x5)

Filtered all non-integer terms:

4373_0_createList_NULL(x1, x2, x3, x4) → 4373_0_createList_NULL(x1, x2, x3)
3040_0_createList_Load(x1, x2, x3, x4) → 3040_0_createList_Load(x1, x2, x4)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, x2) → 3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, +(x2, 1)) | <(x2, x1)
3040_0_createList_Load(EOS(STATIC_3040(x0)), x1, x2) → 3040_0_createList_Load(EOS(STATIC_3040(+(x0, 1))), x1, +(x2, 1)) | &&(<(x2, x1), >(x0, -1))
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, x2) → COND_3040_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3040(x0)), x1, x2)
COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0)), x1, x2) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, +(x2, 1))
3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, x2) → COND_3040_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3040(x0)), x1, x2)
COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0)), x1, x2) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0, 1))), x1, +(x2, 1))
R rules:

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0]) → COND_3040_0_CREATELIST_LOAD(x2[0] < x1[0], EOS(STATIC_3040(x0[0])), x1[0], x2[0])
(1): COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], x2[1] + 1)
(2): 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2]) → COND_3040_0_CREATELIST_LOAD1(x2[2] < x1[2] && x0[2] > -1, EOS(STATIC_3040(x0[2])), x1[2], x2[2])
(3): COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[3] + 1)), x1[3], x2[3] + 1)

(0) -> (1), if (x2[0] < x1[0] ∧EOS(STATIC_3040(x0[0])) →^* EOS(STATIC_3040(x0[1]))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

(1) -> (0), if (EOS(STATIC_3040(x0[1])) →^* EOS(STATIC_3040(x0[0]))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

(1) -> (2), if (EOS(STATIC_3040(x0[1])) →^* EOS(STATIC_3040(x0[2]))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* x2[2])

(2) -> (3), if (x2[2] < x1[2] && x0[2] > -1 ∧EOS(STATIC_3040(x0[2])) →^* EOS(STATIC_3040(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

(3) -> (0), if (EOS(STATIC_3040(x0[3] + 1)) →^* EOS(STATIC_3040(x0[0]))∧x1[3] →^* x1[0]∧x2[3] + 1 →^* x2[0])

(3) -> (2), if (EOS(STATIC_3040(x0[3] + 1)) →^* EOS(STATIC_3040(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

The set Q is empty.

(30) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@1b32991a Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, x2) → COND_3040_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3040(x0)), x1, x2) the following chains were created:

We consider the chain 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0]) → COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0]), COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:
(1)    (<(x2[0], x1[0])=TRUE∧EOS(STATIC_3040(x0[0]))=EOS(STATIC_3040(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0])≥NonInfC∧3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0])≥COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (<(x2[0], x1[0])=TRUE ⇒ 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0])≥NonInfC∧3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0])≥COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(8)    (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

(9)    (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

For Pair COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0)), x1, x2) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:
(10)    (COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1])≥NonInfC∧COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1])≥3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))∧(U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))), ≥))

We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(11)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(12)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(13)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(14)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

For Pair 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, x2) → COND_3040_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3040(x0)), x1, x2) the following chains were created:

We consider the chain 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2]) → COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2]), COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:
(15)    (&&(<(x2[2], x1[2]), >(x0[2], -1))=TRUE∧EOS(STATIC_3040(x0[2]))=EOS(STATIC_3040(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2])≥NonInfC∧3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2])≥COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (15) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(16)    (<(x2[2], x1[2])=TRUE∧>(x0[2], -1)=TRUE ⇒ 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2])≥NonInfC∧3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2])≥COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(17)    (x1[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[2] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    (x1[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[2] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    (x1[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[2] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(20)    (x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(21)    (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

(22)    (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

For Pair COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0)), x1, x2) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0, 1))), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:
(23)    (COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3])≥3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))∧(U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(26)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(27)    ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, x2) → COND_3040_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3040(x0)), x1, x2)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0)), x1, x2) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, +(x2, 1))
- ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)
3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0)), x1, x2) → COND_3040_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3040(x0)), x1, x2)
- (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
- (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0)), x1, x2) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0, 1))), x1, +(x2, 1))
- ((U^Increasing(3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(3040_0_CREATELIST_LOAD(x₁, x₂, x₃)) = [-1]x₃ + x₂
POL(EOS(x₁)) = x₁
POL(STATIC_3040(x₁)) = x₁
POL(COND_3040_0_CREATELIST_LOAD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₃
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_3040_0_CREATELIST_LOAD1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₃
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]

The following pairs are in P_>:

3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0]) → COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])
3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2]) → COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])

The following pairs are in P_bound:

3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[0])), x1[0], x2[0]) → COND_3040_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3040(x0[0])), x1[0], x2[0])
3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[2])), x1[2], x2[2]) → COND_3040_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3040(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], +(x2[1], 1))
COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(+(x0[3], 1))), x1[3], +(x2[3], 1))

There are no usable rules.

(31) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_3040_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3040(x0[1])), x1[1], x2[1]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[1])), x1[1], x2[1] + 1)
(3): COND_3040_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3040(x0[3])), x1[3], x2[3]) → 3040_0_CREATELIST_LOAD(EOS(STATIC_3040(x0[3] + 1)), x1[3], x2[3] + 1)

The set Q is empty.

(32) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Complex Obligation (AND)

(10) Obligation:

(11) IDependencyGraphProof (EQUIVALENT transformation)

(12) TRUE

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPtoQDPProof (SOUND transformation)

(20) Obligation:

(21) UsableRulesProof (EQUIVALENT transformation)

(22) Obligation:

(23) QReductionProof (EQUIVALENT transformation)

(24) Obligation:

(25) QDPSizeChangeProof (EQUIVALENT transformation)

(26) YES

(27) Obligation:

(28) SCCToIDPv1Proof (SOUND transformation)

(29) Obligation:

(30) IDPNonInfProof (SOUND transformation)

(31) Obligation:

(32) IDependencyGraphProof (EQUIVALENT transformation)

(33) TRUE